(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: ListInt
/**
* A set of functions over lists of integers.
*
* All calls terminate.
*
* Julia + BinTerm prove that all calls terminate
*
* Note that cyclicity is introduced by the statement
* <tt>l1.tail.tail = l1</tt>. However, this is not enough to induce
* non-termination in the program. If you instead uncomment the line
* <tt>l0.tail.tail = l0</tt>, most of the calls cannot be proved to terminate
* anymore.
*
* @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A>
*/

public class ListInt {
private int head;
private ListInt tail;

public static void main(String[] args) {
ListInt l0 = new ListInt(5,new ListInt(6,null));
ListInt l1 = new ListInt(1,new ListInt(3,null));
l0.merge(l1);
l1.tail.tail = l1;
//l0.tail.tail = l0;
l0.append(l1);
l0.iter();
l0.reverseAcc(null);
l0.reverse();
}

public ListInt(int head, ListInt tail) {
this.head = head;
this.tail = tail;
}

private void iter() {
if (tail != null) tail.iter();
}

private ListInt append(ListInt other) {
if (tail == null) return new ListInt(head,other);
else return new ListInt(head,tail.append(other));
}

private ListInt reverseAcc(ListInt acc) {
if (tail == null) return new ListInt(head,acc);
else return tail.reverseAcc(new ListInt(head,acc));
}

private ListInt reverse() {
if (tail == null) return this;
else return tail.reverse().append(new ListInt(head,null));
}

private ListInt merge(ListInt other) {
if (other == null) return this;
else if (head <= other.head)
if (tail != null) return new ListInt(head,tail.merge(other));
else return new ListInt(head,other);
else return new ListInt(other.head,merge(other.tail));
}
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
ListInt.main([Ljava/lang/String;)V: Graph of 277 nodes with 0 SCCs.


(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

(4) TRUE